package com.googlecode.kipler.syntax.concept;

import com.googlecode.kipler.syntax.LTLBinaryOperator;


public class LTLBinaryConcept extends Concept {

	private LTLBinaryOperator constructor;

	private Concept lhs, rhs;

	public LTLBinaryConcept() {

	}

	public LTLBinaryConcept(LTLBinaryOperator constructor, Concept lhs, Concept rhs) {
		super();
		this.constructor = constructor;
		this.lhs = lhs;
		this.rhs = rhs;
	}

	public LTLBinaryOperator getConstructor() {
		return constructor;
	}

	public Concept getLhs() {
		return lhs;
	}

	public void setLhs(Concept lhs) {
		this.lhs = lhs;
	}

	public Concept getRhs() {
		return rhs;
	}

	public void setRhs(Concept rhs) {
		this.rhs = rhs;
	}

	public void setConstructor(LTLBinaryOperator constructor) {
		this.constructor = constructor;
	}

	@Override
	public boolean isNegated() {
		return false;
	}

	@Override
	public Concept toggleNegated() {
		if (getConstructor().equals(LTLBinaryOperator.UNTIL)) {
			setConstructor(LTLBinaryOperator.BEFORE);
		} else {
			setConstructor(LTLBinaryOperator.UNTIL);
		}
		setLhs(getLhs().toggleNegated());
		// rhs remains the same
		return this;
	}

	@Override
	public void accept(ConceptVisitor v) {
		v.visitLTLBinaryConcept(this);
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			LTLBinaryConcept other = (LTLBinaryConcept) obj;
			return (this.getConstructor().equals(other.getConstructor())
					&& this.getLhs().equals(other.getLhs()) && this.getRhs()
					.equals(other.getRhs()));
		}
		return false;
	}

	@Override
	public int hashCode() {
		return 17 * 37 + super.hashCode() + getConstructor().hashCode()
				+ getLhs().hashCode() + getRhs().hashCode();
	}

	public LTLBinaryConcept copy() {
		LTLBinaryConcept result = new LTLBinaryConcept();
		result.setConstructor(getConstructor());
		result.setLhs(getLhs().copy());
		result.setRhs(getRhs().copy());
		return result;
	}

	/**
	 * @see java.lang.Object#toString()
	 */
	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append("(");
		buffer.append(getLhs());
		if (getConstructor() == LTLBinaryOperator.UNTIL)
			buffer.append(" U ");
		else
			buffer.append(" B ");
		buffer.append(getRhs());
		buffer.append(")");
		return buffer.toString();
	}

}
